Inference at * 1 
Iof proof for Lemma mul bounds 1b:



1. a : 
2. b : 
  0 < (a * b) 

latex

 by Assert (a * 0) < (a * b) 

latex

 1: .....assertion..... NILNIL

 1:   (a * 0) < (a * b)
 2: 

 2: 3. (a * 0) < (a * b)
 2:   0 < (a * b)
 .

Definitions

a < b, #$n, n * m